M:MsgA, k:Knd, x:Id. M:k may not read x  M.rframe(k reads x) 

latex

Definitions	False, t  T, Id, Knd, type List, x.A(x), P  Q, x:A. B(x), x. t(x), f(x), KindDeq, deq-member(eq;x;L), b, x:AB(x), Prop, A, Void, P  Q, P & Q, P  Q, True, b, , Top, a:A fp B(a), s = t, x:AB(x), Unit, left+right, z != f(x)  P(a;z), M.rframe(k reads x), MsgA, M:k may not read x, IdDeq, x  dom(f), (x  l), Type, {T}
Lemmas	iff functionality wrt iff, not functionality wrt iff, implies functionality wrt iff, assert-deq-member, l member wf, msga wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, fpf-dom wf, fpf-trivial-subtype-top, bool wf, bnot wf, true wf, not wf, false wf, assert wf, deq-member wf, Kind-deq wf, fpf-ap wf, Knd wf, Id wf, id-deq wf